'">
参考文献
戸次 大介; "数理論理学"
西村 祐輝; "Kripke Frameの性質とTableauの停止性"
T. Bolander, Patrick Blackburn; "Termination for hybrid tableaus"
T. Bolandar, Patrick Blackburn; "Termination teblaeu calculi for hybrid logics extending K"
Memo
直観主義命題論理の完全性定理では古典論理のように極大無矛盾集合を構成すると失敗する(二重否定除去が無いから)
ので,少し違う方法で構成する.
プライム性という概念を考える.
Memo
https://github.com/arakur/ProofHSI
Tarski の高校代数問題の反例である Wilkie の等式と,Burris-Yean の構成した 12 要素の有限モデルについて,Lean4 を用いて形式検証しました.
Tarskiの高校代数問題に関するLean 4での形式化
https://github.com/leanprover/lean4/issues/3270
@[deprecated] theorem Nat.deprfl (n : Nat) : n = n := rfl
-- expected: deprecation warning
example {n : Nat} : n = n := Nat.deprfl n
-- unexpected: no deprecation warning
lean-jaが管理しているLean 4のタクティクの一覧
https://lean-ja.github.io/tactic-cheatsheet/index.html
Lean 4の成果物をちゃんとGitHub Actionsでチェックしたいとき,Mathlibをちゃんとキャッシュしないととんでもないことになる.
FormalizedFormalLogic/Foundationに対して追加したこのファイルを参考にしてほしい.
https://github.com/iehality/lean4-logic/blob/ab047c4b1167c9459eecf3cc341c09c9f3503cea/.github/workflows/ci.yml
古典命題論理における含意を演算子として予め持っているプログラミング言語及び…
Nix
https://nixos.wiki/wiki/Nix_Expression_Language#Operators
14, IMPL
e1 -> e2
https://github.com/JLimperg/aesop
White-box automation for Lean 4
概要
Lean 4の証明を一部自動化する便利なタクティクaesop
を追加する.
Automated Extensible Search for Obvious Proofs
2022年ではLean 4
#定理証明支援系
メモ
ページ内リンクとしてはLean Theorem Proverのほうがいいかもしれない
キャッシュについて
Lean 4で書かれた証明/コードをGitHub Actionsでビルドするとき何をキャッシュすれば良いのか調べたが,よくわからなかった.
elanを導入すればLakeが勝手に入ってくるのでlake build
とすればいい.
問題はlake build
はMathlib4とかに依存しているとバカみたいに長いということがあり…
素朴に考えれば/lake-packages
と/build
をキャッシュすればいい
参考文献
Lean 4
leanprover/std4
Mathlib4
Lean 4
参考文献
藤田 博司『原始帰納的函数とアッカーマン函数』
http://tenasaku.com/academia/notes/ackermann-20120302.pdf
論理と計算のしくみ(本)
Lean 4及びMathlib4上でははここにある